(DEFPROP ITERDEF 
 (LAMBDA NIL
  (PROG (CCL INVS IBAL IVAL IGAL VARS)
	(RETURN
	 (LIST (QUOTE DEFPROP)
 	       OP
	       (APPEND (LIST (QUOTE THCONSE))
		       (LIST
			(APPEND (SETQ VARS (VARLIST
				 (APPEND (GET OP (QUOTE IBAS))
					 (GET OP (QUOTE INVAR))
					 (GET OP (QUOTE ISTEP))
					 (GET OP (QUOTE IG)))))
(QUOTE (INASS NAMES FT NT CGL LCTR LWF LUF PS PB BP SASSERTLITS INVAR1 INVAR2 CTST))))
		       (LIST
			(SETQ G
			      (CONS (CAAR (LAST (CAR (GET OP (QUOTE IG)))))
				    (APPEND (ARGLIST (CDAR (LAST (CAR (GET OP (QUOTE IG)))))) (QUOTE (R))))))
		       (LIST (QUOTE (THSETQ (THV LCTR) (THV GCTR))))
		       (COND (BTSW (CONTRLTRACE (CDR (REVERSE (CDR (REVERSE G)))))) (T NIL))
		       (COND (STAT (LIST (QUOTE (SETQ THME (ADD1 THME))))) (T NIL))
		       (LIST (LIST (QUOTE TREEPATH) OP G))
		       (COND
			((GET OP (QUOTE ASSUM))
			 (LIST
			  (LIST (QUOTE THSETQ)
				(QUOTE (THV ASSL))
				(LIST (QUOTE CONS) (LIST (QUOTE QUOTE) OP) (QUOTE (THV ASSL)))))))
		       (COND (TRACESW
			      (LIST (QUOTE (TRACEINFO1)) (LIST (QUOTE THOR) T (LIST (QUOTE TRACEINFO2) OP))))
			     (T NIL))
		       (LIST
			(LIST (QUOTE COND) (LIST (LIST (QUOTE TTYIN)) (LIST (QUOTE ADVICESYS))) (QUOTE (T T))))
		       (QUOTE
			((THSETQ (THV LWF) NIL T T) (THCOND ((NOT (THV WF)) (THSETQ (THV LWF) T)) (T T))
						    (THSETQ (THV WF) T)
						    (THSETQ (THV LUF) NIL T T)
						    (THSETQ (THV PS) (EVAL (CAR (THV ANS))) T T)
						    (THSET (CAR (THV ANS)) NIL)))
		       (REJECTQUIK ((LAMBDA (Y) (COND ((EQ Y T) NIL) (T Y))) (GET OP (QUOTE IBAS))) NIL)
		       (CSG (SUBGOALCOND ((LAMBDA (Y) (COND ((EQ Y T) NIL) (T Y))) (GET OP (QUOTE IBAS))) NIL))
		       (QUOTE ((THSETQ (THV BP) (EVAL (CAR (THV ANS))) T T) (THSET (CAR (THV ANS)) NIL)))
		       (COND
			((NOT (GET OP (QUOTE OA)))
			 (QUOTE ((THCOND ((THV UF) (THSETQ (THV PB) NIL T T) (THGO UP1)) (T T)))))
			(T NIL))
		       (QUOTE ((THOR T (THFAIL THEOREM))))
		       (QUOTE (REP))
		     (SETQ INVS (GENINVAR (GET OP (QUOTE INVAR)) NIL))
		     (SETUP_INASS_NAMES VARS)
		     (GENINVAR* (GET OP (QUOTE INVAR)) NIL)
(LIST(LIST @THSETQ @(THV CTST)(CONS @LIST
(CONS (LIST @QUOTE(CAAAR(GET OP @ICT)))
    (CDR(PLPRED(CAAR(GET OP @ICT))T))))))

		       (QUOTE ((THOR T (THFAIL THEOREM))))
		       (QUOTE ((THSETQ (THV SASSERTLITS) (THV ASSERTLITS) T T)))
		       (PRINT(REJECTQUIK (GET OP (QUOTE ISTEP)) NIL))
 		       (PRINT(CSG (PRINT(SUBGOALCOND (GET OP (QUOTE ISTEP)) NIL))))
 		       (RESETCHNGVARS IVAL)
 		       INVS
 		       (QUOTE ((THSETQ (THV PB) (EVAL (CAR (THV ANS))) T T)))
~		       (LIST (LIST (QUOTE THSETQ) (QUOTE (THV INVAR2)) (CONS (QUOTE LIST) CCL) T T))
~		       (QUOTE
~			((THCOND ((THASVAL (THV FT))
~				  (THSETQ (THV NT)
~					  (COMPCHANGES (THV INVAR1)
~						       (THV INVAR2)
~						       (INCRELIT (THV SASSERTLITS)
~								 (REVERSE (THV ASSERTLITS))))))
~				 (T
~				  (THSETQ (THV FT)
~					  (COMPCHANGES (THV INVAR1)
~						       (THV INVAR2)
~						       (INCRELIT (THV SASSERTLITS)
~								 (REVERSE (THV ASSERTLITS)))))))))
~		       (LIST
~			(LIST (QUOTE THCOND)
~			      (APPEND (LIST
~				       (LIST (QUOTE AND)
~					     (LIST (QUOTE NOT) (QUOTE (THASVAL (THV NT))))
~					     (LIST (QUOTE AMBIG) (QUOTE (THV FT)))))
~				      (RESETCHNGVARS IVAL)
~				      (QUOTE ((THSET (CAR (THV ANS)) NIL) (THGO REP))))
~			      (QUOTE (T T))))
		       (QUOTE((SETQ GTEMP
			         (WHILASSEM
				     (THV BP)
				     (THV PB)
				     (CONS(THV NAMES)(THV INASS))
				     (THV INVAR1)
				     (THV CTST)))))
		       (QUOTE ((THSETQ (THV PB) GTEMP T T)))
		       (COND ((GET OP (QUOTE OA)) (IASSERTUP (GET OP (QUOTE OA)))) (T (UNWINDUP)))
		       (QUOTE
			((SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
			 (THCOND ((THV LWF) (THSETQ (THV WF) NIL T T)
					    (THSETQ (THV BT) NIL T T)
					    (SETQ GANS (REMBT GANS)))
				 (T T))
			 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
			 (THCOND ((THV LUF) (THSETQ (THV UF) NIL T T) (THSETQ (THV ULS) T)) (T T))))
		       (LIST
			(LIST (QUOTE THCOND)
			      (LIST (QUOTE (THV ULS))
				    (LIST (QUOTE THSETQ)
					  (QUOTE (THV ASSERTLITS))
					  (LIST (QUOTE CONS)
						(LIST (QUOTE LIST)
						      (APPEND (QUOTE (LIST))
							      (LIST
							       (LIST (QUOTE QUOTE)
								     (CAR
								      (PLPRED
								       (CAR (LAST (CAR (GET OP (QUOTE IG)))))
								       NIL))))
							      (CDR
							       (PLPRED (CAR (LAST (CAR (GET OP (QUOTE IG)))))
 								       T))
							      (QUOTE ((QUOTE R))))
						      (CONS (QUOTE LIST)
							    (UNEVALARG
							     (CDR (CAR (LAST (CAR (GET OP (QUOTE IG)))))))))
						(QUOTE (THV ASSERTLITS)))))
			      (LIST T
				    (LIST (QUOTE THSETQ)
					  (QUOTE (THV WASSERTLITS))
					  (LIST (QUOTE CONS)
						(LIST (QUOTE LIST)
						      (APPEND (QUOTE (LIST))
							      (LIST
							       (LIST (QUOTE QUOTE)
								     (CAR
								      (PLPRED
								       (CAR (LAST (CAR (GET OP (QUOTE IG)))))
								       NIL))))
							      (CDR
							       (PLPRED (CAR (LAST (CAR (GET OP (QUOTE IG)))))
 								       T))
							      (QUOTE ((QUOTE R))))
						      (CONS (QUOTE LIST)
							    (UNEVALARG
							     (CDR (CAR (LAST (CAR (GET OP (QUOTE IG)))))))))
						(QUOTE (THV WASSERTLITS)))))))
		       (QUOTE ((COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))))
	       (QUOTE THEOREM))))) 
EXPR)